FDL - Nuprl Definition : es-ek

Nuprl Definition : es-ek

0,22

e=k(v).P(e;v) ==

e:E. kind(e) = k & P(e;val(e))

clarification:

es-ek(es; k; e,v.P(e;v)) ==

e:es-E(es). es-kind(es; e) = k

Knd & P(e;es-val(es; e))

Definitions e=k(v).P(e;v), x:A. B(x), E, P & Q, Knd, kind(e), val(e)

FDL editor aliases es-ek

Definitions	e=k(v).P(e;v), x:A. B(x), E, P & Q, Knd, kind(e), val(e)
FDL editor aliases	es-ek